Step of Proof: can-apply-fun-exp 11,40
Inference at * 
Iof proof for Lemma can-apply-fun-exp:


  A:Type, f:(A(A + Top)), n:, y:A.
  (can-apply(f^n;y))  (m:. (m  n)  (can-apply(f^m;y))) 
latex
 by (Unfold `can-apply` ( 0)) 
CollapseTHEN (((InductionOnNat) 
CollapseTHEN (Auto)) 

CoCollapseTHEN ((CaseNat 0 `m') 
CollapseTHEN (((Try ((RepUR ``p-fun-exp p-compose p-id`` ( 0)) 

CoCollapseTHEN (Trivial)))) 
CollapseTHEN ((Subst' m ~ ((m - 1)+1) ( 0)) 
CollapseTHEN ((
C(Try ((Complete (Auto'))))) 
CollapseTHEN ((RWO "p-fun-exp-add" 0) 
CollapseTHEN ((Auto) 

CoCollapseTHEN ((MoveToConcl (-4)) 
CollapseTHEN ((Subst' n ~ ((n - 1)+1) ( 0)) 
CollapseTHEN ((
C(Try ((Complete (Auto'))))) 
CollapseTHEN ((RWO "p-fun-exp-add" 0) 
CollapseTHENA (Auto)))
C))))))))) 
latex

C1: 

C1: 1. A : Type
C1: 2. f : A(A + Top)
C1: 3. n : 
C1: 4. 0 < n
C1: 5. y:A. (isl(f^n - 1(y)))  (m:. (m  (n - 1))  (isl(f^m(y))))
C1: 6. y : A
C1: 7. m : 
C1: 8. m  n
C1: 9. (m = 0)
C1:   (isl(f^n - 1 o f^1  (y)))  (isl(f^m - 1 o f^1  (y)))
C.

Definitionss ~ t, n+m, n - m, #$n, i  j , can-apply(f;x), Dec(P), P  Q, s = t, p-id(), SQType(T), {T}, P  Q, P & Q, x:A  B(x), , left + right, T, P  Q, True, , Type, b, isl(x), Top, f(a), f o g  , f^n, , {x:A| B(x)} , , A, False, P  Q, x:AB(x), Void, a < b, -n, A  B, x:A. B(x), t  T
Lemmasge wf, nat properties, nat wf, top wf, decidable int equal, nat sq, bool wf, squash wf, true wf, p-fun-exp-add, assert wf, isl wf, p-compose wf, p-fun-exp wf, le wf

origin